# Copyright 2024 Google LLC
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#      http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

load("@com_google_googleapis_imports//:imports.bzl", "cc_proto_library")

package(
    default_visibility = ["//visibility:public"],
    licenses = ["notice"],
)

cc_library(
    name = "util",
    srcs = ["util.cc"],
    hdrs = ["util.h"],
    deps = [
        "//gutil/gutil:status",
        "//p4_pdpi/netaddr:ipv6_address",
        "//p4_pdpi/string_encodings:decimal_string",
        "//p4_pdpi/utils:ir",
        "//p4_symbolic:z3_util",
	"//p4_symbolic/sai",
        "//p4_symbolic/symbolic",
        "//p4_symbolic/symbolic:operators",
        "//p4_symbolic/symbolic:solver_state",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
    ],
)

proto_library(
    name = "packet_synthesis_criteria_proto",
    srcs = ["packet_synthesis_criteria.proto"],
    deps = ["//p4_pdpi:ir_proto"],
)

cc_proto_library(
    name = "packet_synthesis_criteria_cc_proto",
    deps = [":packet_synthesis_criteria_proto"],
)

proto_library(
    name = "packet_synthesizer_proto",
    srcs = ["packet_synthesizer.proto"],
    deps = [
        ":packet_synthesis_criteria_proto",
        "//p4_pdpi/packetlib:packetlib_proto",
        "@com_github_p4lang_p4runtime//:p4runtime_proto",
    ],
)

proto_library(
    name = "coverage_goal_proto",
    srcs = ["coverage_goal.proto"],
    deps = [
        ":packet_synthesis_criteria_proto",
    ],
)

cc_proto_library(
    name = "coverage_goal_cc_proto",
    deps = [":coverage_goal_proto"],
)

cc_proto_library(
    name = "packet_synthesizer_cc_proto",
    deps = [":packet_synthesizer_proto"],
)

cc_library(
    name = "packet_synthesis_criteria",
    srcs = ["packet_synthesis_criteria.cc"],
    hdrs = ["packet_synthesis_criteria.h"],
    deps = [
        ":packet_synthesis_criteria_cc_proto",
        "//gutil/gutil:status",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_test(
    name = "packet_synthesis_criteria_test",
    srcs = ["packet_synthesis_criteria_test.cc"],
    deps = [
        ":packet_synthesis_criteria",
        ":packet_synthesis_criteria_cc_proto",
        "//gutil/gutil:proto_matchers",
        "//gutil/gutil:status_matchers",
        "//gutil/gutil:testing",
        "@com_google_absl//absl/status",
        "@com_google_googletest//:gtest_main",
    ],
)

cc_library(
    name = "packet_synthesizer",
    srcs = ["packet_synthesizer.cc"],
    hdrs = ["packet_synthesizer.h"],
    deps = [
        ":packet_synthesis_criteria",
        ":packet_synthesis_criteria_cc_proto",
        ":packet_synthesizer_cc_proto",
        ":util",
        ":z3_model_to_packet",
        "//gutil/gutil:status",
        "//gutil/gutil:timer",
        "//p4_pdpi:ir_cc_proto",
        "//p4_symbolic/ir:ir_cc_proto",
        "//p4_symbolic/symbolic",
        "//p4_symbolic/symbolic:solver_state",
        "//p4_symbolic/symbolic:values",
        "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/memory",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/time",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "criteria_generator",
    srcs = ["criteria_generator.cc"],
    hdrs = ["criteria_generator.h"],
    deps = [
        ":coverage_goal_cc_proto",
        ":packet_synthesis_criteria",
        ":packet_synthesis_criteria_cc_proto",
        "//gutil/gutil:proto",
        "//p4_pdpi:ir_cc_proto",
        "//p4_symbolic/ir:ir_cc_proto",
        "//p4_symbolic/symbolic",
        "//p4_symbolic/symbolic:solver_state",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
    ],
)

cc_library(
    name = "z3_model_to_packet",
    srcs = ["z3_model_to_packet.cc"],
    hdrs = ["z3_model_to_packet.h"],
    deps = [
        ":packet_synthesizer_cc_proto",
        "//p4_pdpi/packetlib",
        "//p4_symbolic:z3_util",
        "//p4_symbolic/sai",
        "//p4_symbolic/symbolic:solver_state",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:string_view",
    ],
)
